package be.ac.info.fundp.TVLParser.Util;

import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.Vector;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.ModelIterator;
import org.sat4j.tools.SolutionCounter;

import be.ac.info.fundp.TVLParser.SyntaxTree.AndExpression;
import be.ac.info.fundp.TVLParser.SyntaxTree.BooleanExpression;
import be.ac.info.fundp.TVLParser.SyntaxTree.ParenthesesExpression;
import be.ac.info.fundp.TVLParser.exceptions.UnsatisfiableModelException;
import be.ac.info.fundp.TVLParser.symbolTables.FeatureSymbol;

/**
 * An object from this class allows to compute different operations about a feature model. This feature model
 * has to be normalized and converted into its boolean form.
 *
 */
public class Solver {
	
	//The solver
	private ISolver sat4JSolver;
	
	private int timeout = 60;
	
	// A vector which contains each dimacs clauses generated by the constraints, the cardinalities and  the
	// justification rules of the feature model.
	private Vector<int[]> numericalClauses = new Vector<int[]>();
	
	
	// Constructor :
	// -------------

	/**
	 * This constructor builds a new solver. It creates a new ISolver object and initializes it with "timeout".
	 * The different constraints of "rootFeatureSymbol" are converted into the DIMACS format and added to 
	 * "chocoSolver". The constraints of the cardinalities and the features justification rules are also generated 
	 * into the DIMACS format and added to "sat4JSolver".
	 * 
	 * @param rootFeatureSymbol
	 * 		The root feature of the feature model on which the solver will work. If this feature model 
	 * 		has'nt been normalized and convert into it's boolean form, this constructor will crash.
	 * 
	 * @exception ContradictionException
	 * 		If there is contradiction between two boolean clauses.
	 * 
	 * @exception UnsatisfiableModelException
	 * 		If the feature model is unsatisfiable.
	 * 
	 */
	public Solver(FeatureSymbol rootFeatureSymbol) throws ContradictionException, UnsatisfiableModelException {
		sat4JSolver  = SolverFactory.newDefault();
		sat4JSolver.setTimeout(timeout);
		textualCNFToDIMACS(BooleanForm.mergeConstraints(rootFeatureSymbol));
		cardinalitiesAndJustificationRulesToDIMACS(rootFeatureSymbol);
	}
	
	// Methods used by the constructor :
	// ---------------------------------
	
	/**
	 *  This method re-initializes "sat4JSolver" and replaces it by a new iSolver using the dimacs formulas 
	 *  contained in "numericalClauses".
	 *  
	 *  Because of a bug in the SAT4J library, this method is launched each time a solver operation is made.
	 */
	public void reInitializeSolver() {
		ISolver newSolver = SolverFactory.newDefault();
		newSolver.setTimeout(timeout);
		int i = 0;
		while (i <= this.numericalClauses.size()-1) {
			try {
				newSolver.addClause(new VecInt(this.numericalClauses.get(i)));
			} catch (ContradictionException e) {
				// Normally, this exception is never thrown.
				e.printStackTrace();
			}
			i++;
		}
		this.sat4JSolver = newSolver;
	}
	
	/**
	 * This method converts a CNF formula into its DIMACS format. Each clause is transformed into an int array
	 * and added to "sat4JSolver" and "numericalClauses".
	 * 
	 * @param booleanExpression
	 * 		The CNF formula which will be convert into its DIMACS format and added to "sat4JSolver".
	 * 
	 * @exception ContradictionException
	 * 		If there is contradiction between the generated DIMACS formula and a clause contained in "sat4JSolver".
	 * 
	 * @exception UnsatisfiableModelException
	 * 		If the feature model is unsatisfiable.
	 * 
	 */
	/*private void textualCNFToDIMACS(BooleanExpression booleanExpression) throws ContradictionException, UnsatisfiableModelException {
		if (booleanExpression != null) {
			Vector<BooleanExpression> constraintsClauses = new Vector<BooleanExpression>();
			constraintsClauses = BooleanForm.toClausesVector(booleanExpression, constraintsClauses); 
			int i = 0;
			while (i <= constraintsClauses.size()-1) {
				int[] clause = BooleanForm.toNumericalClause(constraintsClauses.get(i));
				if (clause != null) {
					if ((clause.length == 1) && (clause[0] == -1)) {
						throw new UnsatisfiableModelException("Solver error : the feature model is unsatisfiable.");
					}
					else {
						this.sat4JSolver.addClause(new VecInt(clause));
						this.numericalClauses.add(clause);
					}
				}
				i++;
			}
		}
	}*/
	
	/**
	 * This method :
	 * 	1) Generates the cardinalities constraints and the justification rules (into CNF) of "featureSymbol".
	 * 	   This method is also called for each child of "featureSymbol".
	 * 	2) Transforms these new CNF formulas into the DIMACS format.
	 * 	3) Adds each DIMACS clause to "sat4JSolver" and "numericalClauses."
	 * 
	 * @param featureSymbol
	 * 		The feature symbol for which the cardinalities constraints and the justification rules will be generated.
	 * 
	 * @exception ContradictionException
	 * 		If there is contradiction between the generated DIMACS formulas and a clause contained in "sat4JSolver".
	 */
	private void cardinalitiesAndJustificationRulesToDIMACS(FeatureSymbol featureSymbol) throws ContradictionException {
		if (featureSymbol != null && featureSymbol.hasChildrenFeatures()) {
			int[][] cardinalityConstraintClauses =  BooleanForm.generateCNFRules(featureSymbol);
			int i = 0;
			while (i <= cardinalityConstraintClauses.length-1) {
				sat4JSolver.addClause(new VecInt(cardinalityConstraintClauses[i]));
				this.numericalClauses.add(cardinalityConstraintClauses[i]);
				i++;
			}
			i = 0;
			Object[] childrenFeaturesSymbol = featureSymbol.getChildrenFeatures().keySet().toArray();
			FeatureSymbol childrenFeatureSymbol;
			while (i <= childrenFeaturesSymbol.length-1) {
				childrenFeatureSymbol = featureSymbol.getChildrenFeature(childrenFeaturesSymbol[i].toString());
				cardinalitiesAndJustificationRulesToDIMACS(childrenFeatureSymbol);
				i++;
			}
		}
		int[] featureJustificationRulesClause = BooleanForm.generateFeatureJustificationRule(featureSymbol);
		sat4JSolver.addClause(new VecInt(featureJustificationRulesClause));
		this.numericalClauses.add(featureJustificationRulesClause);
	}
	
	/**
	 * This method converts a CNF formula into its DIMACS format. Each clause is transformed into an int array
	 * and added to "sat4JSolver" and "numericalClauses". If "booleanExpression" is null, do nothing.
	 * 
	 * @param booleanExpression
	 * 		The CNF formula which will be convert into its DIMACS format and added to "sat4JSolver".
	 *  
	 * @exception ContradictionException
	 * 		If there is contradiction between the generated DIMACS formula and a clause contained in "sat4JSolver".
	 * 
	 * @exception UnsatisfiableModelException
	 * 		If the feature model is unsatisfiable.
	 */
	public void textualCNFToDIMACS(BooleanExpression booleanExpression) throws UnsatisfiableModelException, ContradictionException {
		if (booleanExpression != null) {
			if (booleanExpression instanceof AndExpression) {
				textualCNFToDIMACS((BooleanExpression) ((AndExpression) booleanExpression).getExpression1());
				textualCNFToDIMACS((BooleanExpression) ((AndExpression) booleanExpression).getExpression2());
			}
			else {
				while (booleanExpression instanceof ParenthesesExpression) {
					booleanExpression = (BooleanExpression) ((ParenthesesExpression) booleanExpression).getExpression();
				}
				int[] clause = BooleanForm.toNumericalClause(booleanExpression);
				if (clause != null) {
					if ((clause.length == 1) && (clause[0] == -1)) {
						throw new UnsatisfiableModelException("Solver error : the feature model is unsatisfiable.");
					}
					else {
						this.sat4JSolver.addClause(new VecInt(clause));
						this.numericalClauses.add(clause);
					}
				}
			}
		}
	}
	

	// Solver state modification methods :
	// -----------------------------------
	
	/**
	 * Sets the timeout of "sat4JSolver". Default timeout is 60 sec.
	 * 
	 * @param nbrSec
	 *            The new timeout.
	 */
	public void setTimeout(int nbrSec) {
		this.timeout = nbrSec;
	}


	// Solving methods :
	// -----------------

	/**
	 * Shows if the clauses contained into the SAT4J solver are satisfiable or not.
	 * 
	 * @return True if all the clauses contained into the sat4J solver can be satisfied.
	 * 
	 * @throws TimeoutException
	 *             Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public boolean isSatisfiable() throws TimeoutException {
			return sat4JSolver.isSatisfiable();
	}

	
	public boolean isSatisfiable(int ID) throws TimeoutException {
			return sat4JSolver.isSatisfiable(new VecInt(new int[] { ID }));
	}
	
	public boolean isSatisfiable(IVecInt assumptions) throws TimeoutException {
		return sat4JSolver.isSatisfiable(assumptions);	
	}
	/**
	 * Shows if the given id does not appear in any solution.
	 * 
	 * @return True if the given id does not appear in any solution
	 * 
	 * @throws TimeoutException
	 *             Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public boolean isDead(int ID) throws TimeoutException {
		boolean isDead = !sat4JSolver.isSatisfiable(new VecInt(new int[] { ID }));
		this.reInitializeSolver();
		return isDead;
	}

	/**
	 * Count the number of solutions which satisfies the clauses contained into the sat4J solver. 
	 * Be careful, artificial variables are also included into the computing. So, the solutions number
	 * can be erroneous.
	 * 
	 * @return The number of solutions which satisfies the clauses contained into sat4J solver.
	 * 
	 * @throws TimeoutException
	 *            Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public long countSolutions() throws TimeoutException {
		SolutionCounter cpt = new SolutionCounter(sat4JSolver);
		Long solutionsNumber = cpt.countSolutions();
		this.reInitializeSolver();
		return solutionsNumber;
	}

	/**
	 * Count the number of solutions which contains the given ID. Be careful, artificial variables 
	 * are also included into the computing. So, the solutions number can be erroneous.
	 * 
	 * @return The number of solutions which contains the given ID.
	 * 
	 * @throws TimeoutException
	 *            Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public long countSolutions(int ID) throws TimeoutException {
		try {
			ISolver solver = this.sat4JSolver;
			solver.addAtLeast(new VecInt(new int[] { ID }), 1);
			SolutionCounter cpt = new SolutionCounter(solver);
			long solutionsNumber = cpt.countSolutions();
			this.reInitializeSolver();
			return solutionsNumber;
		} catch (ContradictionException e) {
			e.printStackTrace();
			return 0;
		}
	}

	/**
	 * Return all the solutions which satisfies the clauses contained into the SAT4J solver. 
	 * 
	 * @return An array of int arrays containing all the solutions which satisfies the clauses 
	 * contained into "sat4JSolver"
	 * 
	 * @throws TimeoutException
	 *           Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public int[][] getAllSolutions() throws TimeoutException {
		ModelIterator modelIt = null;
		ISolver tempSolver = sat4JSolver;
		modelIt = new ModelIterator(tempSolver);
		ArrayList<int[]> solutions = new ArrayList<int[]>();
		int[] aModel;

		// Iterate over the solutions other solver
		while (modelIt.isSatisfiable()) {
			aModel = modelIt.model();
			solutions.add(aModel);
		}
		this.reInitializeSolver();
		return solutions.toArray(new int[solutions.size()][]);
	}

	/**
	 * Return all the solutions which contains the given ID.
	 * 
	 * @return An array of int arrays containing all the solutions which includes
	 * the given ID.
	 * 
	 * @throws TimeoutException
	 *           Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public int[][] getAllSolutions(int featureId) throws TimeoutException {
		ModelIterator modelIt = null;
		try {
			ISolver solver = this.sat4JSolver;
			solver.addAtLeast(new VecInt(new int[] { featureId }), 1);
			modelIt = new ModelIterator(solver);
		} catch (ContradictionException e) {
			e.printStackTrace();
			return null;
		}
		ArrayList<int[]> solutions = new ArrayList<int[]>();
		int[] aModel;

		// Iterate over the solutions other solver
		while (modelIt.isSatisfiable()) {
			aModel = modelIt.model();
			solutions.add(aModel);
		}
		this.reInitializeSolver();
		return solutions.toArray(new int[solutions.size()][]);
	}

	/**
	 * Return one solution which satisfies all the clauses of the sat4J solver.
	 * 
	 * @return An int array representing a solution.
	 * 
	 * @throws TimeoutException
	 *           Launched by "sat4JSolver" if "timeOut" has been exceeded.
	 */
	public int[] getOneSolutions() throws TimeoutException {
		ISolver tempSolver = sat4JSolver;
		ModelIterator modelIt = new ModelIterator(tempSolver); 
		int[] aModel = new int[0];
		// If there is a solutions
		if (modelIt.isSatisfiable()) {
			aModel = modelIt.model();
		}
		this.reInitializeSolver();
		return aModel;
	}
	
	public void addClause(int clause) throws ContradictionException {
		this.sat4JSolver.addClause(new VecInt(new int[] { clause })) ;
	}
	
	@SuppressWarnings("unchecked")
	public void removeUnitClause(int clause) {
	//	((org.sat4j.minisat.core.Solver)this.sat4JSolver).undo(clause);
	}
	
	@SuppressWarnings("unchecked")
	public String toString(){
		org.sat4j.minisat.core.Solver zzs = (org.sat4j.minisat.core.Solver) this.sat4JSolver ;
		ILits voc = zzs.getVocabulary();
		String s="";
		for(int i=0; i<voc.nVars(); i++) {
			if(!voc.isUnassigned(i))
				s += "\n"+i+" = "+ voc.isSatisfied(i) ;
		}
		return s ;
	}
	
	public List<List<Integer>> explain(int id, List<Integer> state) throws TimeoutException {
	     // return ((Xplain<ISolver>)this.sat4JSolver).explain() ;
		List<List<Integer>> result = new ArrayList<List<Integer>>();
		int i=0;
		int j=0;
		int lit=0;
		boolean relevant = false;
		org.sat4j.minisat.core.Solver solver = (org.sat4j.minisat.core.Solver) this.sat4JSolver;
				
		
		IConstr constr = solver.getIthConstr(i++);
		
		while(constr != null) {
			relevant = false;
			j = 0;
			while(!relevant && j < constr.size()) {
				lit = constr.get(j++);
				if(lit == solver.getVocabulary().getFromPool(id) || lit == solver.getVocabulary().getFromPool(-id)) {
					relevant = true ;
				}
			}
			if(relevant) {
				boolean idWasAsSpecified = (lit == solver.getVocabulary().getFromPool(id));
				ArrayList<Integer> theConstr = new ArrayList<Integer>();
				j = 0;
				while(!idWasAsSpecified && j < constr.size()) {
					lit = constr.get(j++);
					int dimacsId = (lit % 2 ==0) ? (lit / 2) : -((lit-1)/2) ; 
					if(dimacsId != Math.abs(id)) {
						// Si idWasAsSpecified est false, alors on doit trouver une valeur qui contredit
							if(state.contains(Integer.valueOf(-dimacsId))) {
									theConstr.add(dimacsId);		
							}
						
					}
				}
				if(theConstr.size() > 0) result.add(theConstr) ;
			}
			
			constr = solver.getIthConstr(i++);
		}
		
		return result ;
	}
	
	/**
	 * Stores this.numericalClauses in a text file.
	 * @param filepath defines the (absolute or relative) filepath to the target file.
	 * @return true iff the writing ended successfully.
	 */
	public boolean storeDimacsClauses(String filepath, int varsNbr) {
		try {
			PrintWriter pw =  new PrintWriter(new BufferedWriter(new FileWriter(filepath)));
			pw.println("p cnf "+varsNbr+" "+numericalClauses.size());
			for (int i = 0; i < numericalClauses.size(); i++) {
				for (int j = 0; j < numericalClauses.get(i).length; j++)
					pw.print(numericalClauses.get(i)[j]+" ");
				pw.println(0);
			}
			pw.close();
			return true;
		}
		catch(IOException e) {
			System.out.println("Could not store the clauses in the file "+filepath+".\n");
			return false;
		}
	}
	
}